YES 57.133
↳ HASKELL
↳ LR
((minusFM :: FiniteMap () a -> FiniteMap () b -> FiniteMap () a) :: FiniteMap () a -> FiniteMap () b -> FiniteMap () a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord a => FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMax :: Ord b => FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMin :: Ord b => FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueVBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
minusFM :: Ord c => FiniteMap c a -> FiniteMap c b -> FiniteMap c a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap b a -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
\(mid_key1,_)→mid_key1
mid_key10 (mid_key1,_) = mid_key1
\(_,mid_elt1)→mid_elt1
mid_elt10 (_,mid_elt1) = mid_elt1
\(mid_key2,_)→mid_key2
mid_key20 (mid_key2,_) = mid_key2
\(_,mid_elt2)→mid_elt2
mid_elt20 (_,mid_elt2) = mid_elt2
\oldnew→new
addToFM0 old new = new
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
((minusFM :: FiniteMap () b -> FiniteMap () a -> FiniteMap () b) :: FiniteMap () b -> FiniteMap () a -> FiniteMap () b) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord a => FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMax :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMin :: Ord b => FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueBal :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueVBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
minusFM :: Ord c => FiniteMap c b -> FiniteMap c a -> FiniteMap c b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
case fm_l of EmptyFM → True Branch left_key _ _ _ _ →
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
left_ok0 fm_l key EmptyFM = True left_ok0 fm_l key (Branch left_key _ _ _ _) =
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
case fm_r of EmptyFM → True Branch right_key _ _ _ _ →
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
right_ok0 fm_r key EmptyFM = True right_ok0 fm_r key (Branch right_key _ _ _ _) =
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
case fm_R of Branch _ _ _ fm_rl fm_rr
| sizeFM fm_rl < 2 * sizeFM fm_rr
→ single_L fm_L fm_R | otherwise
→ double_L fm_L fm_R
mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
case fm_L of Branch _ _ _ fm_ll fm_lr
| sizeFM fm_lr < 2 * sizeFM fm_ll
→ single_R fm_L fm_R | otherwise
→ double_R fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
((minusFM :: FiniteMap () a -> FiniteMap () b -> FiniteMap () a) :: FiniteMap () a -> FiniteMap () b -> FiniteMap () a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord a => FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMax :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMin :: Ord b => FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueBal :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueVBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
minusFM :: Ord c => FiniteMap c b -> FiniteMap c a -> FiniteMap c b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
fm_l@(Branch yx yy yz zu zv)
Branch yx yy yz zu zv
fm_r@(Branch zx zy zz vuu vuv)
Branch zx zy zz vuu vuv
fm_l@(Branch vux vuy vuz vvu vvv)
Branch vux vuy vuz vvu vvv
fm_r@(Branch vvx vvy vvz vwu vwv)
Branch vvx vvy vvz vwu vwv
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((minusFM :: FiniteMap () a -> FiniteMap () b -> FiniteMap () a) :: FiniteMap () a -> FiniteMap () b -> FiniteMap () a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMax :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMin :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueBal :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueVBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
minusFM :: Ord b => FiniteMap b a -> FiniteMap b c -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap b a -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
splitLT EmptyFM split_key = emptyFM splitLT (Branch key elt xw fm_l fm_r) split_key
| split_key < key
= splitLT fm_l split_key | split_key > key
= mkVBalBranch key elt fm_l (splitLT fm_r split_key) | otherwise
= fm_l
splitLT EmptyFM split_key = splitLT4 EmptyFM split_key splitLT (Branch key elt xw fm_l fm_r) split_key = splitLT3 (Branch key elt xw fm_l fm_r) split_key
splitLT1 key elt xw fm_l fm_r split_key True = mkVBalBranch key elt fm_l (splitLT fm_r split_key) splitLT1 key elt xw fm_l fm_r split_key False = splitLT0 key elt xw fm_l fm_r split_key otherwise
splitLT2 key elt xw fm_l fm_r split_key True = splitLT fm_l split_key splitLT2 key elt xw fm_l fm_r split_key False = splitLT1 key elt xw fm_l fm_r split_key (split_key > key)
splitLT0 key elt xw fm_l fm_r split_key True = fm_l
splitLT3 (Branch key elt xw fm_l fm_r) split_key = splitLT2 key elt xw fm_l fm_r split_key (split_key < key)
splitLT4 EmptyFM split_key = emptyFM splitLT4 wvw wvx = splitLT3 wvw wvx
splitGT EmptyFM split_key = emptyFM splitGT (Branch key elt xx fm_l fm_r) split_key
| split_key > key
= splitGT fm_r split_key | split_key < key
= mkVBalBranch key elt (splitGT fm_l split_key) fm_r | otherwise
= fm_r
splitGT EmptyFM split_key = splitGT4 EmptyFM split_key splitGT (Branch key elt xx fm_l fm_r) split_key = splitGT3 (Branch key elt xx fm_l fm_r) split_key
splitGT1 key elt xx fm_l fm_r split_key True = mkVBalBranch key elt (splitGT fm_l split_key) fm_r splitGT1 key elt xx fm_l fm_r split_key False = splitGT0 key elt xx fm_l fm_r split_key otherwise
splitGT2 key elt xx fm_l fm_r split_key True = splitGT fm_r split_key splitGT2 key elt xx fm_l fm_r split_key False = splitGT1 key elt xx fm_l fm_r split_key (split_key < key)
splitGT0 key elt xx fm_l fm_r split_key True = fm_r
splitGT3 (Branch key elt xx fm_l fm_r) split_key = splitGT2 key elt xx fm_l fm_r split_key (split_key > key)
splitGT4 EmptyFM split_key = emptyFM splitGT4 wwu wwv = splitGT3 wwu wwv
glueVBal EmptyFM fm2 = fm2 glueVBal fm1 EmptyFM = fm1 glueVBal (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv)
| sIZE_RATIO * size_l < size_r
= mkBalBranch zx zy (glueVBal (Branch yx yy yz zu zv) vuu) vuv | sIZE_RATIO * size_r < size_l
= mkBalBranch yx yy zu (glueVBal zv (Branch zx zy zz vuu vuv)) | otherwise
= glueBal (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv) where
size_l = sizeFM (Branch yx yy yz zu zv)
size_r = sizeFM (Branch zx zy zz vuu vuv)
glueVBal EmptyFM fm2 = glueVBal5 EmptyFM fm2 glueVBal fm1 EmptyFM = glueVBal4 fm1 EmptyFM glueVBal (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv) = glueVBal3 (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv)
glueVBal3 (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv) =
glueVBal2 yx yy yz zu zv zx zy zz vuu vuv (sIZE_RATIO * size_l < size_r) where
glueVBal0 yx yy yz zu zv zx zy zz vuu vuv True = glueBal (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv)
glueVBal1 yx yy yz zu zv zx zy zz vuu vuv True = mkBalBranch yx yy zu (glueVBal zv (Branch zx zy zz vuu vuv)) glueVBal1 yx yy yz zu zv zx zy zz vuu vuv False = glueVBal0 yx yy yz zu zv zx zy zz vuu vuv otherwise
glueVBal2 yx yy yz zu zv zx zy zz vuu vuv True = mkBalBranch zx zy (glueVBal (Branch yx yy yz zu zv) vuu) vuv glueVBal2 yx yy yz zu zv zx zy zz vuu vuv False = glueVBal1 yx yy yz zu zv zx zy zz vuu vuv (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch yx yy yz zu zv)
size_r = sizeFM (Branch zx zy zz vuu vuv)
glueVBal4 fm1 EmptyFM = fm1 glueVBal4 wwz wxu = glueVBal3 wwz wxu
glueVBal5 EmptyFM fm2 = fm2 glueVBal5 wxw wxx = glueVBal4 wxw wxx
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
| sIZE_RATIO * size_l < size_r
= mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv | sIZE_RATIO * size_r < size_l
= mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv)) | otherwise
= mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) where
size_l = sizeFM (Branch vux vuy vuz vvu vvv)
size_r = sizeFM (Branch vvx vvy vvz vwu vwv)
mkVBalBranch key elt EmptyFM fm_r = mkVBalBranch5 key elt EmptyFM fm_r mkVBalBranch key elt fm_l EmptyFM = mkVBalBranch4 key elt fm_l EmptyFM mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) =
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_l < size_r) where
mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv)) mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch vux vuy vuz vvu vvv)
size_r = sizeFM (Branch vvx vvy vvz vwu vwv)
mkVBalBranch4 key elt fm_l EmptyFM = addToFM fm_l key elt mkVBalBranch4 wyv wyw wyx wyy = mkVBalBranch3 wyv wyw wyx wyy
mkVBalBranch5 key elt EmptyFM fm_r = addToFM fm_r key elt mkVBalBranch5 wzu wzv wzw wzx = mkVBalBranch4 wzu wzv wzw wzx
mkBalBranch1 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr)
mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vwz vxu vxv fm_ll fm_lr otherwise
mkBalBranch10 fm_L fm_R vwz vxu vxv fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch12 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch0 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
mkBalBranch0 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vyu vyv vyw fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vyu vyv vyw fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch key elt fm_L fm_R
| size_l + size_r < 2
= mkBranch 1 key elt fm_L fm_R | size_r > sIZE_RATIO * size_l
= mkBalBranch0 fm_L fm_R fm_R | size_l > sIZE_RATIO * size_r
= mkBalBranch1 fm_L fm_R fm_L | otherwise
= mkBranch 2 key elt fm_L fm_R where
double_L fm_l (Branch key_r elt_r vxy (Branch key_rl elt_rl vxz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxw fm_ll (Branch key_lr elt_lr vxx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r vyx fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vwy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R
mkBalBranch6 key elt fm_L fm_R =
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where
double_L fm_l (Branch key_r elt_r vxy (Branch key_rl elt_rl vxz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxw fm_ll (Branch key_lr elt_lr vxx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vyu vyv vyw fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vyu vyv vyw fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vwz vxu vxv fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vwz vxu vxv fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vyx fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vwy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
glueBal EmptyFM fm2 = fm2 glueBal fm1 EmptyFM = fm1 glueBal fm1 fm2
| sizeFM fm2 > sizeFM fm1
= mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2) | otherwise
= mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2 where
mid_elt1 = mid_elt10 vv2
mid_elt10 (vyy,mid_elt1) = mid_elt1
mid_elt2 = mid_elt20 vv3
mid_elt20 (vyz,mid_elt2) = mid_elt2
mid_key1 = mid_key10 vv2
mid_key10 (mid_key1,vzu) = mid_key1
mid_key2 = mid_key20 vv3
mid_key20 (mid_key2,vzv) = mid_key2
vv2 = findMax fm1
vv3 = findMin fm2
glueBal EmptyFM fm2 = glueBal4 EmptyFM fm2 glueBal fm1 EmptyFM = glueBal3 fm1 EmptyFM glueBal fm1 fm2 = glueBal2 fm1 fm2
glueBal2 fm1 fm2 =
glueBal1 fm1 fm2 (sizeFM fm2 > sizeFM fm1) where
glueBal0 fm1 fm2 True = mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2
glueBal1 fm1 fm2 True = mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2) glueBal1 fm1 fm2 False = glueBal0 fm1 fm2 otherwise
mid_elt1 = mid_elt10 vv2
mid_elt10 (vyy,mid_elt1) = mid_elt1
mid_elt2 = mid_elt20 vv3
mid_elt20 (vyz,mid_elt2) = mid_elt2
mid_key1 = mid_key10 vv2
mid_key10 (mid_key1,vzu) = mid_key1
mid_key2 = mid_key20 vv3
mid_key20 (mid_key2,vzv) = mid_key2
vv2 = findMax fm1
vv3 = findMin fm2
glueBal3 fm1 EmptyFM = fm1 glueBal3 xuv xuw = glueBal2 xuv xuw
glueBal4 EmptyFM fm2 = fm2 glueBal4 xuy xuz = glueBal3 xuy xuz
addToFM_C combiner EmptyFM key elt = unitFM key elt addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt
| new_key < key
= mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r | new_key > key
= mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt) | otherwise
= Branch new_key (combiner elt new_elt) size fm_l fm_r
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt) addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)
addToFM_C4 combiner EmptyFM key elt = unitFM key elt addToFM_C4 xvw xvx xvy xvz = addToFM_C3 xvw xvx xvy xvz
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
((minusFM :: FiniteMap () b -> FiniteMap () a -> FiniteMap () b) :: FiniteMap () b -> FiniteMap () a -> FiniteMap () b) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord a => FiniteMap a b -> a -> b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMax :: Ord a => FiniteMap a b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
deleteMin :: Ord b => FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
glueVBal :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
minusFM :: Ord c => FiniteMap c a -> FiniteMap c b -> FiniteMap c a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where
double_L fm_l (Branch key_r elt_r vxy (Branch key_rl elt_rl vxz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxw fm_ll (Branch key_lr elt_lr vxx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vyu vyv vyw fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vyu vyv vyw fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vyu vyv vyw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vwz vxu vxv fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vwz vxu vxv fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vwz vxu vxv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vyx fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vwy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
mkBalBranch6Double_R xwu xwv xww xwx (Branch key_l elt_l vxw fm_ll (Branch key_lr elt_lr vxx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 xwu xwv fm_lrr fm_r)
mkBalBranch6MkBalBranch1 xwu xwv xww xwx fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch6MkBalBranch12 xwu xwv xww xwx fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr)
mkBalBranch6MkBalBranch12 xwu xwv xww xwx fm_L fm_R (Branch vwz vxu vxv fm_ll fm_lr) = mkBalBranch6MkBalBranch11 xwu xwv xww xwx fm_L fm_R vwz vxu vxv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch6Size_r xwu xwv xww xwx = sizeFM xww
mkBalBranch6Double_L xwu xwv xww xwx fm_l (Branch key_r elt_r vxy (Branch key_rl elt_rl vxz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 xwu xwv fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
mkBalBranch6MkBalBranch3 xwu xwv xww xwx key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 xwu xwv xww xwx fm_L fm_R fm_L mkBalBranch6MkBalBranch3 xwu xwv xww xwx key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 xwu xwv xww xwx key elt fm_L fm_R otherwise
mkBalBranch6MkBalBranch5 xwu xwv xww xwx key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch6MkBalBranch5 xwu xwv xww xwx key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 xwu xwv xww xwx key elt fm_L fm_R (mkBalBranch6Size_r xwu xwv xww xwx > sIZE_RATIO * mkBalBranch6Size_l xwu xwv xww xwx)
mkBalBranch6Size_l xwu xwv xww xwx = sizeFM xwx
mkBalBranch6MkBalBranch02 xwu xwv xww xwx fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch6MkBalBranch01 xwu xwv xww xwx fm_L fm_R vyu vyv vyw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch6Single_R xwu xwv xww xwx (Branch key_l elt_l vwy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 xwu xwv fm_lr fm_r)
mkBalBranch6MkBalBranch4 xwu xwv xww xwx key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 xwu xwv xww xwx fm_L fm_R fm_R mkBalBranch6MkBalBranch4 xwu xwv xww xwx key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 xwu xwv xww xwx key elt fm_L fm_R (mkBalBranch6Size_l xwu xwv xww xwx > sIZE_RATIO * mkBalBranch6Size_r xwu xwv xww xwx)
mkBalBranch6MkBalBranch10 xwu xwv xww xwx fm_L fm_R vwz vxu vxv fm_ll fm_lr True = mkBalBranch6Double_R xwu xwv xww xwx fm_L fm_R
mkBalBranch6MkBalBranch2 xwu xwv xww xwx key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch6MkBalBranch00 xwu xwv xww xwx fm_L fm_R vyu vyv vyw fm_rl fm_rr True = mkBalBranch6Double_L xwu xwv xww xwx fm_L fm_R
mkBalBranch6Single_L xwu xwv xww xwx fm_l (Branch key_r elt_r vyx fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 xwu xwv fm_l fm_rl) fm_rr
mkBalBranch6MkBalBranch01 xwu xwv xww xwx fm_L fm_R vyu vyv vyw fm_rl fm_rr True = mkBalBranch6Single_L xwu xwv xww xwx fm_L fm_R mkBalBranch6MkBalBranch01 xwu xwv xww xwx fm_L fm_R vyu vyv vyw fm_rl fm_rr False = mkBalBranch6MkBalBranch00 xwu xwv xww xwx fm_L fm_R vyu vyv vyw fm_rl fm_rr otherwise
mkBalBranch6MkBalBranch0 xwu xwv xww xwx fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr) = mkBalBranch6MkBalBranch02 xwu xwv xww xwx fm_L fm_R (Branch vyu vyv vyw fm_rl fm_rr)
mkBalBranch6MkBalBranch11 xwu xwv xww xwx fm_L fm_R vwz vxu vxv fm_ll fm_lr True = mkBalBranch6Single_R xwu xwv xww xwx fm_L fm_R mkBalBranch6MkBalBranch11 xwu xwv xww xwx fm_L fm_R vwz vxu vxv fm_ll fm_lr False = mkBalBranch6MkBalBranch10 xwu xwv xww xwx fm_L fm_R vwz vxu vxv fm_ll fm_lr otherwise
glueVBal2 yx yy yz zu zv zx zy zz vuu vuv (sIZE_RATIO * size_l < size_r) where
glueVBal0 yx yy yz zu zv zx zy zz vuu vuv True = glueBal (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv)
glueVBal1 yx yy yz zu zv zx zy zz vuu vuv True = mkBalBranch yx yy zu (glueVBal zv (Branch zx zy zz vuu vuv)) glueVBal1 yx yy yz zu zv zx zy zz vuu vuv False = glueVBal0 yx yy yz zu zv zx zy zz vuu vuv otherwise
glueVBal2 yx yy yz zu zv zx zy zz vuu vuv True = mkBalBranch zx zy (glueVBal (Branch yx yy yz zu zv) vuu) vuv glueVBal2 yx yy yz zu zv zx zy zz vuu vuv False = glueVBal1 yx yy yz zu zv zx zy zz vuu vuv (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch yx yy yz zu zv)
size_r = sizeFM (Branch zx zy zz vuu vuv)
glueVBal3GlueVBal2 xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv yx yy yz zu zv zx zy zz vuu vuv True = mkBalBranch zx zy (glueVBal (Branch yx yy yz zu zv) vuu) vuv glueVBal3GlueVBal2 xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv yx yy yz zu zv zx zy zz vuu vuv False = glueVBal3GlueVBal1 xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv yx yy yz zu zv zx zy zz vuu vuv (sIZE_RATIO * glueVBal3Size_r xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv < glueVBal3Size_l xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv)
glueVBal3Size_r xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv = sizeFM (Branch xwy xwz xxu xxv xxw)
glueVBal3GlueVBal0 xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv yx yy yz zu zv zx zy zz vuu vuv True = glueBal (Branch yx yy yz zu zv) (Branch zx zy zz vuu vuv)
glueVBal3GlueVBal1 xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv yx yy yz zu zv zx zy zz vuu vuv True = mkBalBranch yx yy zu (glueVBal zv (Branch zx zy zz vuu vuv)) glueVBal3GlueVBal1 xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv yx yy yz zu zv zx zy zz vuu vuv False = glueVBal3GlueVBal0 xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv yx yy yz zu zv zx zy zz vuu vuv otherwise
glueVBal3Size_l xwy xwz xxu xxv xxw xxx xxy xxz xyu xyv = sizeFM (Branch xxx xxy xxz xyu xyv)
glueVBal (minusFM lts left) (minusFM gts right) where
gts = splitGT fm1 split_key
lts = splitLT fm1 split_key
minusFMGts xyw xyx = splitGT xyw xyx
minusFMLts xyw xyx = splitLT xyw xyx
let
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r in result where
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True left_ok0 fm_l key (Branch left_key wu wv ww wx) =
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True right_ok0 fm_r key (Branch right_key vw vx vy vz) =
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
right_size = sizeFM fm_r
unbox x = x
mkBranchBalance_ok xyy xyz xzu = True
mkBranchUnbox xyy xyz xzu x = x
mkBranchRight_ok0 xyy xyz xzu fm_r key EmptyFM = True mkBranchRight_ok0 xyy xyz xzu fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r
mkBranchRight_size xyy xyz xzu = sizeFM xyy
mkBranchRight_ok xyy xyz xzu = mkBranchRight_ok0 xyy xyz xzu xyy xyz xyy
mkBranchLeft_size xyy xyz xzu = sizeFM xzu
mkBranchLeft_ok0 xyy xyz xzu fm_l key EmptyFM = True mkBranchLeft_ok0 xyy xyz xzu fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key
mkBranchLeft_ok xyy xyz xzu = mkBranchLeft_ok0 xyy xyz xzu xzu xyz xzu
let
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r in result
mkBranchResult xzv xzw xzx xzy = Branch xzv xzw (mkBranchUnbox xzx xzv xzy (1 + mkBranchLeft_size xzx xzv xzy + mkBranchRight_size xzx xzv xzy)) xzy xzx
glueBal1 fm1 fm2 (sizeFM fm2 > sizeFM fm1) where
glueBal0 fm1 fm2 True = mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2
glueBal1 fm1 fm2 True = mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2) glueBal1 fm1 fm2 False = glueBal0 fm1 fm2 otherwise
mid_elt1 = mid_elt10 vv2
mid_elt10 (vyy,mid_elt1) = mid_elt1
mid_elt2 = mid_elt20 vv3
mid_elt20 (vyz,mid_elt2) = mid_elt2
mid_key1 = mid_key10 vv2
mid_key10 (mid_key1,vzu) = mid_key1
mid_key2 = mid_key20 vv3
mid_key20 (mid_key2,vzv) = mid_key2
vv2 = findMax fm1
vv3 = findMin fm2
glueBal2Mid_key2 xzz yuu = glueBal2Mid_key20 xzz yuu (glueBal2Vv3 xzz yuu)
glueBal2Vv3 xzz yuu = findMin xzz
glueBal2Mid_elt10 xzz yuu (vyy,mid_elt1) = mid_elt1
glueBal2Mid_elt20 xzz yuu (vyz,mid_elt2) = mid_elt2
glueBal2Mid_elt2 xzz yuu = glueBal2Mid_elt20 xzz yuu (glueBal2Vv3 xzz yuu)
glueBal2Mid_key10 xzz yuu (mid_key1,vzu) = mid_key1
glueBal2GlueBal1 xzz yuu fm1 fm2 True = mkBalBranch (glueBal2Mid_key2 xzz yuu) (glueBal2Mid_elt2 xzz yuu) fm1 (deleteMin fm2) glueBal2GlueBal1 xzz yuu fm1 fm2 False = glueBal2GlueBal0 xzz yuu fm1 fm2 otherwise
glueBal2Mid_elt1 xzz yuu = glueBal2Mid_elt10 xzz yuu (glueBal2Vv2 xzz yuu)
glueBal2Mid_key20 xzz yuu (mid_key2,vzv) = mid_key2
glueBal2Vv2 xzz yuu = findMax yuu
glueBal2Mid_key1 xzz yuu = glueBal2Mid_key10 xzz yuu (glueBal2Vv2 xzz yuu)
glueBal2GlueBal0 xzz yuu fm1 fm2 True = mkBalBranch (glueBal2Mid_key1 xzz yuu) (glueBal2Mid_elt1 xzz yuu) (deleteMax fm1) fm2
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_l < size_r) where
mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv)) mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch vux vuy vuz vvu vvv)
size_r = sizeFM (Branch vvx vvy vvz vwu vwv)
mkVBalBranch3MkVBalBranch0 yuv yuw yux yuy yuz yvu yvv yvw yvx yvy key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
mkVBalBranch3MkVBalBranch2 yuv yuw yux yuy yuz yvu yvv yvw yvx yvy key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv mkVBalBranch3MkVBalBranch2 yuv yuw yux yuy yuz yvu yvv yvw yvx yvy key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch1 yuv yuw yux yuy yuz yvu yvv yvw yvx yvy key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * mkVBalBranch3Size_r yuv yuw yux yuy yuz yvu yvv yvw yvx yvy < mkVBalBranch3Size_l yuv yuw yux yuy yuz yvu yvv yvw yvx yvy)
mkVBalBranch3MkVBalBranch1 yuv yuw yux yuy yuz yvu yvv yvw yvx yvy key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv)) mkVBalBranch3MkVBalBranch1 yuv yuw yux yuy yuz yvu yvv yvw yvx yvy key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch0 yuv yuw yux yuy yuz yvu yvv yvw yvx yvy key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise
mkVBalBranch3Size_l yuv yuw yux yuy yuz yvu yvv yvw yvx yvy = sizeFM (Branch yuv yuw yux yuy yuz)
mkVBalBranch3Size_r yuv yuw yux yuy yuz yvu yvv yvw yvx yvy = sizeFM (Branch yvu yvv yvw yvx yvy)
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
mkBranchRight_ok0Smallest_right_key yvz = fst (findMin yvz)
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
mkBranchLeft_ok0Biggest_left_key ywu = fst (findMax ywu)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
((minusFM :: FiniteMap () b -> FiniteMap () a -> FiniteMap () b) :: FiniteMap () b -> FiniteMap () a -> FiniteMap () b) |
import qualified Maybe import qualified Prelude |
|||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
deleteMax :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||
deleteMin :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
|||||||||||||
glueBal :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
glueVBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
minusFM :: Ord b => FiniteMap b a -> FiniteMap b c -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> a ( -> (FiniteMap a b) (Int -> Int)))
|
|||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
(minusFM :: FiniteMap () a -> FiniteMap () b -> FiniteMap () a) |
import qualified Maybe import qualified Prelude |
|||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||
addToFM :: Ord a => FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
deleteMax :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||
deleteMin :: Ord a => FiniteMap a b -> FiniteMap a b
|
|||||||||||||
emptyFM :: FiniteMap b a
|
|||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||
glueBal :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
glueVBal :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
minusFM :: Ord b => FiniteMap b a -> FiniteMap b c -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> a ( -> (FiniteMap a b) (Int -> Int)))
|
|||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt10(ywv1128, ywv1129, ywv1130, ywv1131, ywv1132, ywv1133, ywv1134, ywv1135, ywv1136, ywv1137, ywv1138, ywv1139, Branch(ywv11400, ywv11401, ywv11402, ywv11403, ywv11404), h, ba) → new_glueBal2Mid_elt10(ywv1128, ywv1129, ywv1130, ywv1131, ywv1132, ywv1133, ywv1134, ywv1135, ywv11400, ywv11401, ywv11402, ywv11403, ywv11404, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key10(ywv1114, ywv1115, ywv1116, ywv1117, ywv1118, ywv1119, ywv1120, ywv1121, ywv1122, ywv1123, ywv1124, ywv1125, Branch(ywv11260, ywv11261, ywv11262, ywv11263, ywv11264), h, ba) → new_glueBal2Mid_key10(ywv1114, ywv1115, ywv1116, ywv1117, ywv1118, ywv1119, ywv1120, ywv1121, ywv11260, ywv11261, ywv11262, ywv11263, ywv11264, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt20(ywv942, ywv943, ywv944, ywv945, ywv946, ywv947, ywv948, ywv949, ywv950, ywv951, ywv952, Branch(ywv9530, ywv9531, ywv9532, ywv9533, ywv9534), ywv954, h, ba) → new_glueBal2Mid_elt20(ywv942, ywv943, ywv944, ywv945, ywv946, ywv947, ywv948, ywv949, ywv9530, ywv9531, ywv9532, ywv9533, ywv9534, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key20(ywv926, ywv927, ywv928, ywv929, ywv930, ywv931, ywv932, ywv933, ywv934, ywv935, ywv936, Branch(ywv9370, ywv9371, ywv9372, ywv9373, ywv9374), ywv938, h, ba) → new_glueBal2Mid_key20(ywv926, ywv927, ywv928, ywv929, ywv930, ywv931, ywv932, ywv933, ywv9370, ywv9371, ywv9372, ywv9373, ywv9374, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt100(ywv1189, ywv1190, ywv1191, ywv1192, ywv1193, ywv1194, ywv1195, ywv1196, ywv1197, ywv1198, ywv1199, ywv1200, ywv1201, Branch(ywv12020, ywv12021, ywv12022, ywv12023, ywv12024), h, ba) → new_glueBal2Mid_elt100(ywv1189, ywv1190, ywv1191, ywv1192, ywv1193, ywv1194, ywv1195, ywv1196, ywv1197, ywv12020, ywv12021, ywv12022, ywv12023, ywv12024, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key100(ywv1174, ywv1175, ywv1176, ywv1177, ywv1178, ywv1179, ywv1180, ywv1181, ywv1182, ywv1183, ywv1184, ywv1185, ywv1186, Branch(ywv11870, ywv11871, ywv11872, ywv11873, ywv11874), h, ba) → new_glueBal2Mid_key100(ywv1174, ywv1175, ywv1176, ywv1177, ywv1178, ywv1179, ywv1180, ywv1181, ywv1182, ywv11870, ywv11871, ywv11872, ywv11873, ywv11874, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt200(ywv973, ywv974, ywv975, ywv976, ywv977, ywv978, ywv979, ywv980, ywv981, ywv982, ywv983, ywv984, Branch(ywv9850, ywv9851, ywv9852, ywv9853, ywv9854), ywv986, h, ba) → new_glueBal2Mid_elt200(ywv973, ywv974, ywv975, ywv976, ywv977, ywv978, ywv979, ywv980, ywv981, ywv9850, ywv9851, ywv9852, ywv9853, ywv9854, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key200(ywv958, ywv959, ywv960, ywv961, ywv962, ywv963, ywv964, ywv965, ywv966, ywv967, ywv968, ywv969, Branch(ywv9700, ywv9701, ywv9702, ywv9703, ywv9704), ywv971, h, ba) → new_glueBal2Mid_key200(ywv958, ywv959, ywv960, ywv961, ywv962, ywv963, ywv964, ywv965, ywv966, ywv9700, ywv9701, ywv9702, ywv9703, ywv9704, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt101(ywv1100, ywv1101, ywv1102, ywv1103, ywv1104, ywv1105, ywv1106, ywv1107, ywv1108, ywv1109, ywv1110, ywv1111, Branch(ywv11120, ywv11121, ywv11122, ywv11123, ywv11124), h, ba) → new_glueBal2Mid_elt101(ywv1100, ywv1101, ywv1102, ywv1103, ywv1104, ywv1105, ywv1106, ywv1107, ywv11120, ywv11121, ywv11122, ywv11123, ywv11124, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key101(ywv1086, ywv1087, ywv1088, ywv1089, ywv1090, ywv1091, ywv1092, ywv1093, ywv1094, ywv1095, ywv1096, ywv1097, Branch(ywv10980, ywv10981, ywv10982, ywv10983, ywv10984), h, ba) → new_glueBal2Mid_key101(ywv1086, ywv1087, ywv1088, ywv1089, ywv1090, ywv1091, ywv1092, ywv1093, ywv10980, ywv10981, ywv10982, ywv10983, ywv10984, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt201(ywv911, ywv912, ywv913, ywv914, ywv915, ywv916, ywv917, ywv918, ywv919, ywv920, ywv921, Branch(ywv9220, ywv9221, ywv9222, ywv9223, ywv9224), ywv923, h, ba) → new_glueBal2Mid_elt201(ywv911, ywv912, ywv913, ywv914, ywv915, ywv916, ywv917, ywv918, ywv9220, ywv9221, ywv9222, ywv9223, ywv9224, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key201(ywv897, ywv898, ywv899, ywv900, ywv901, ywv902, ywv903, ywv904, ywv905, ywv906, ywv907, Branch(ywv9080, ywv9081, ywv9082, ywv9083, ywv9084), ywv909, h, ba) → new_glueBal2Mid_key201(ywv897, ywv898, ywv899, ywv900, ywv901, ywv902, ywv903, ywv904, ywv9080, ywv9081, ywv9082, ywv9083, ywv9084, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt102(ywv1298, ywv1299, ywv1300, ywv1301, ywv1302, ywv1303, ywv1304, ywv1305, ywv1306, ywv1307, ywv1308, ywv1309, ywv1310, ywv1311, Branch(ywv13120, ywv13121, ywv13122, ywv13123, ywv13124), h, ba) → new_glueBal2Mid_elt102(ywv1298, ywv1299, ywv1300, ywv1301, ywv1302, ywv1303, ywv1304, ywv1305, ywv1306, ywv1307, ywv13120, ywv13121, ywv13122, ywv13123, ywv13124, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key102(ywv1282, ywv1283, ywv1284, ywv1285, ywv1286, ywv1287, ywv1288, ywv1289, ywv1290, ywv1291, ywv1292, ywv1293, ywv1294, ywv1295, Branch(ywv12960, ywv12961, ywv12962, ywv12963, ywv12964), h, ba) → new_glueBal2Mid_key102(ywv1282, ywv1283, ywv1284, ywv1285, ywv1286, ywv1287, ywv1288, ywv1289, ywv1290, ywv1291, ywv12960, ywv12961, ywv12962, ywv12963, ywv12964, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt202(ywv1260, ywv1261, ywv1262, ywv1263, ywv1264, ywv1265, ywv1266, ywv1267, ywv1268, ywv1269, ywv1270, ywv1271, ywv1272, Branch(ywv12730, ywv12731, ywv12732, ywv12733, ywv12734), ywv1274, h, ba) → new_glueBal2Mid_elt202(ywv1260, ywv1261, ywv1262, ywv1263, ywv1264, ywv1265, ywv1266, ywv1267, ywv1268, ywv1269, ywv12730, ywv12731, ywv12732, ywv12733, ywv12734, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key202(ywv1244, ywv1245, ywv1246, ywv1247, ywv1248, ywv1249, ywv1250, ywv1251, ywv1252, ywv1253, ywv1254, ywv1255, ywv1256, Branch(ywv12570, ywv12571, ywv12572, ywv12573, ywv12574), ywv1258, h, ba) → new_glueBal2Mid_key202(ywv1244, ywv1245, ywv1246, ywv1247, ywv1248, ywv1249, ywv1250, ywv1251, ywv1252, ywv1253, ywv12570, ywv12571, ywv12572, ywv12573, ywv12574, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt103(ywv1070, ywv1071, ywv1072, ywv1073, ywv1074, ywv1075, ywv1076, ywv1077, ywv1078, ywv1079, ywv1080, ywv1081, Branch(ywv10820, ywv10821, ywv10822, ywv10823, ywv10824), h, ba) → new_glueBal2Mid_elt103(ywv1070, ywv1071, ywv1072, ywv1073, ywv1074, ywv1075, ywv1076, ywv1077, ywv10820, ywv10821, ywv10822, ywv10823, ywv10824, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key103(ywv1056, ywv1057, ywv1058, ywv1059, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, ywv1065, ywv1066, ywv1067, Branch(ywv10680, ywv10681, ywv10682, ywv10683, ywv10684), h, ba) → new_glueBal2Mid_key103(ywv1056, ywv1057, ywv1058, ywv1059, ywv1060, ywv1061, ywv1062, ywv1063, ywv10680, ywv10681, ywv10682, ywv10683, ywv10684, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt203(ywv882, ywv883, ywv884, ywv885, ywv886, ywv887, ywv888, ywv889, ywv890, ywv891, ywv892, Branch(ywv8930, ywv8931, ywv8932, ywv8933, ywv8934), ywv894, h, ba) → new_glueBal2Mid_elt203(ywv882, ywv883, ywv884, ywv885, ywv886, ywv887, ywv888, ywv889, ywv8930, ywv8931, ywv8932, ywv8933, ywv8934, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key203(ywv868, ywv869, ywv870, ywv871, ywv872, ywv873, ywv874, ywv875, ywv876, ywv877, ywv878, Branch(ywv8790, ywv8791, ywv8792, ywv8793, ywv8794), ywv880, h, ba) → new_glueBal2Mid_key203(ywv868, ywv869, ywv870, ywv871, ywv872, ywv873, ywv874, ywv875, ywv8790, ywv8791, ywv8792, ywv8793, ywv8794, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt104(ywv1039, ywv1040, ywv1041, ywv1042, ywv1043, ywv1044, ywv1045, ywv1046, ywv1047, ywv1048, ywv1049, ywv1050, ywv1051, Branch(ywv10520, ywv10521, ywv10522, ywv10523, ywv10524), h, ba) → new_glueBal2Mid_elt104(ywv1039, ywv1040, ywv1041, ywv1042, ywv1043, ywv1044, ywv1045, ywv1046, ywv1047, ywv10520, ywv10521, ywv10522, ywv10523, ywv10524, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key104(ywv1024, ywv1025, ywv1026, ywv1027, ywv1028, ywv1029, ywv1030, ywv1031, ywv1032, ywv1033, ywv1034, ywv1035, ywv1036, Branch(ywv10370, ywv10371, ywv10372, ywv10373, ywv10374), h, ba) → new_glueBal2Mid_key104(ywv1024, ywv1025, ywv1026, ywv1027, ywv1028, ywv1029, ywv1030, ywv1031, ywv1032, ywv10370, ywv10371, ywv10372, ywv10373, ywv10374, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt204(ywv853, ywv854, ywv855, ywv856, ywv857, ywv858, ywv859, ywv860, ywv861, ywv862, ywv863, ywv864, Branch(ywv8650, ywv8651, ywv8652, ywv8653, ywv8654), ywv866, h, ba) → new_glueBal2Mid_elt204(ywv853, ywv854, ywv855, ywv856, ywv857, ywv858, ywv859, ywv860, ywv861, ywv8650, ywv8651, ywv8652, ywv8653, ywv8654, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key204(ywv838, ywv839, ywv840, ywv841, ywv842, ywv843, ywv844, ywv845, ywv846, ywv847, ywv848, ywv849, Branch(ywv8500, ywv8501, ywv8502, ywv8503, ywv8504), ywv851, h, ba) → new_glueBal2Mid_key204(ywv838, ywv839, ywv840, ywv841, ywv842, ywv843, ywv844, ywv845, ywv846, ywv8500, ywv8501, ywv8502, ywv8503, ywv8504, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt105(ywv1010, ywv1011, ywv1012, ywv1013, ywv1014, ywv1015, ywv1016, ywv1017, ywv1018, ywv1019, ywv1020, ywv1021, Branch(ywv10220, ywv10221, ywv10222, ywv10223, ywv10224), h, ba) → new_glueBal2Mid_elt105(ywv1010, ywv1011, ywv1012, ywv1013, ywv1014, ywv1015, ywv1016, ywv1017, ywv10220, ywv10221, ywv10222, ywv10223, ywv10224, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key105(ywv988, ywv989, ywv990, ywv991, ywv992, ywv993, ywv994, ywv995, ywv996, ywv997, ywv998, ywv999, Branch(ywv10000, ywv10001, ywv10002, ywv10003, ywv10004), h, ba) → new_glueBal2Mid_key105(ywv988, ywv989, ywv990, ywv991, ywv992, ywv993, ywv994, ywv995, ywv10000, ywv10001, ywv10002, ywv10003, ywv10004, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt205(ywv824, ywv825, ywv826, ywv827, ywv828, ywv829, ywv830, ywv831, ywv832, ywv833, ywv834, Branch(ywv8350, ywv8351, ywv8352, ywv8353, ywv8354), ywv836, h, ba) → new_glueBal2Mid_elt205(ywv824, ywv825, ywv826, ywv827, ywv828, ywv829, ywv830, ywv831, ywv8350, ywv8351, ywv8352, ywv8353, ywv8354, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key205(ywv810, ywv811, ywv812, ywv813, ywv814, ywv815, ywv816, ywv817, ywv818, ywv819, ywv820, Branch(ywv8210, ywv8211, ywv8212, ywv8213, ywv8214), ywv822, h, ba) → new_glueBal2Mid_key205(ywv810, ywv811, ywv812, ywv813, ywv814, ywv815, ywv816, ywv817, ywv8210, ywv8211, ywv8212, ywv8213, ywv8214, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt106(ywv1228, ywv1229, ywv1230, ywv1231, ywv1232, ywv1233, ywv1234, ywv1235, ywv1236, ywv1237, ywv1238, ywv1239, ywv1240, ywv1241, Branch(ywv12420, ywv12421, ywv12422, ywv12423, ywv12424), h, ba) → new_glueBal2Mid_elt106(ywv1228, ywv1229, ywv1230, ywv1231, ywv1232, ywv1233, ywv1234, ywv1235, ywv1236, ywv1237, ywv12420, ywv12421, ywv12422, ywv12423, ywv12424, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key106(ywv1204, ywv1205, ywv1206, ywv1207, ywv1208, ywv1209, ywv1210, ywv1211, ywv1212, ywv1213, ywv1214, ywv1215, ywv1216, ywv1217, Branch(ywv12180, ywv12181, ywv12182, ywv12183, ywv12184), h, ba) → new_glueBal2Mid_key106(ywv1204, ywv1205, ywv1206, ywv1207, ywv1208, ywv1209, ywv1210, ywv1211, ywv1212, ywv1213, ywv12180, ywv12181, ywv12182, ywv12183, ywv12184, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_elt206(ywv1158, ywv1159, ywv1160, ywv1161, ywv1162, ywv1163, ywv1164, ywv1165, ywv1166, ywv1167, ywv1168, ywv1169, ywv1170, Branch(ywv11710, ywv11711, ywv11712, ywv11713, ywv11714), ywv1172, h, ba) → new_glueBal2Mid_elt206(ywv1158, ywv1159, ywv1160, ywv1161, ywv1162, ywv1163, ywv1164, ywv1165, ywv1166, ywv1167, ywv11710, ywv11711, ywv11712, ywv11713, ywv11714, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2Mid_key206(ywv1142, ywv1143, ywv1144, ywv1145, ywv1146, ywv1147, ywv1148, ywv1149, ywv1150, ywv1151, ywv1152, ywv1153, ywv1154, Branch(ywv11550, ywv11551, ywv11552, ywv11553, ywv11554), ywv1156, h, ba) → new_glueBal2Mid_key206(ywv1142, ywv1143, ywv1144, ywv1145, ywv1146, ywv1147, ywv1148, ywv1149, ywv1150, ywv1151, ywv11550, ywv11551, ywv11552, ywv11553, ywv11554, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_primMinusNat(Succ(ywv13270), Succ(ywv132900)) → new_primMinusNat(ywv13270, ywv132900)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_primPlusNat(Succ(ywv573000), Succ(ywv57400)) → new_primPlusNat(ywv573000, ywv57400)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_mkBalBranch6MkBalBranch11(ywv1060, ywv1061, ywv788, ywv10630, ywv10631, ywv10632, ywv10633, ywv10634, Succ(ywv1313000), Succ(ywv132100), h, ba) → new_mkBalBranch6MkBalBranch11(ywv1060, ywv1061, ywv788, ywv10630, ywv10631, ywv10632, ywv10633, ywv10634, ywv1313000, ywv132100, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_mkBalBranch6MkBalBranch3(ywv1060, ywv1061, ywv788, ywv1063, Succ(ywv1053000), Succ(ywv121900), h, ba) → new_mkBalBranch6MkBalBranch3(ywv1060, ywv1061, ywv788, ywv1063, ywv1053000, ywv121900, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_mkBalBranch6MkBalBranch01(ywv1060, ywv1061, ywv7880, ywv7881, ywv7882, ywv7883, ywv7884, ywv1063, Succ(ywv1083000), Succ(ywv127900), h, ba) → new_mkBalBranch6MkBalBranch01(ywv1060, ywv1061, ywv7880, ywv7881, ywv7882, ywv7883, ywv7884, ywv1063, ywv1083000, ywv127900, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_mkBalBranch6MkBalBranch4(ywv1060, ywv1061, ywv788, ywv1063, Succ(ywv939000), Succ(ywv100100), h, ba) → new_mkBalBranch6MkBalBranch4(ywv1060, ywv1061, ywv788, ywv1063, ywv939000, ywv100100, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_mkBalBranch6MkBalBranch5(ywv1060, ywv1061, ywv788, ywv1063, Succ(ywv80200), Succ(ywv80300), h, ba) → new_mkBalBranch6MkBalBranch5(ywv1060, ywv1061, ywv788, ywv1063, ywv80200, ywv80300, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_deleteMax(ywv678, ywv679, ywv680, ywv681, Branch(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824), h, ba) → new_deleteMax(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_deleteMin(ywv1003330, ywv1003331, ywv1003332, Branch(ywv10033330, ywv10033331, ywv10033332, ywv10033333, ywv10033334), ywv1003334, h, ba) → new_deleteMin(ywv10033330, ywv10033331, ywv10033332, ywv10033333, ywv10033334, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2GlueBal1(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, Succ(ywv639000), Succ(ywv638000), h, ba) → new_glueBal2GlueBal1(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, ywv639000, ywv638000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2GlueBal10(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, Succ(ywv653000), Succ(ywv652000), h, ba) → new_glueBal2GlueBal10(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv653000, ywv652000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2GlueBal11(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, Succ(ywv637000), Succ(ywv636000), h, ba) → new_glueBal2GlueBal11(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, ywv637000, ywv636000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2GlueBal12(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, Succ(ywv808000), Succ(ywv807000), h, ba) → new_glueBal2GlueBal12(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, ywv808000, ywv807000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2GlueBal13(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, Succ(ywv635000), Succ(ywv634000), h, ba) → new_glueBal2GlueBal13(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, ywv635000, ywv634000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_glueBal2GlueBal14(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, Succ(ywv633000), Succ(ywv632000), h, ba) → new_glueBal2GlueBal14(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv633000, ywv632000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_glueBal2GlueBal15(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, Succ(ywv631000), Succ(ywv630000), h, ba) → new_glueBal2GlueBal15(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, ywv631000, ywv630000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
new_glueBal2GlueBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv731000), Succ(ywv730000), h, ba) → new_glueBal2GlueBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv731000, ywv730000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
new_glueVBal3GlueVBal27(ywv576, ywv577, Pos(ywv5780), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal24(ywv576, ywv577, ywv5780, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Zero), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, Branch(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824), Succ(ywv7190), Pos(ywv7040), bb, bc) → new_glueVBal3(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824, ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal10(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal29(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Succ(ywv10033200), Zero, bd, be)
new_glueVBal3GlueVBal211(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv10033200), bd, be)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Pos(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Succ(ywv10033200)), Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal25(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc) → new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_glueVBal3Size_l(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc), bb, bc)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Zero), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal212(ywv576, ywv577, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv6830), Zero, bb, bc) → new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_glueVBal3Size_l(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc), bb, bc)
new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Pos(ywv7100), ywv704, bb, bc) → new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_primMulNat0(ywv7100), ywv704, bb, bc)
new_glueVBal3GlueVBal110(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal210(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(Succ(ywv106200)), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal3GlueVBal111(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv106200, ywv10033200, bd, be)
new_glueVBal3GlueVBal21(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal24(ywv576, ywv577, ywv5780, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal18(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv71700), Succ(Succ(ywv704000)), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv71700, ywv704000, bb, bc)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Zero, Succ(ywv7010), cb, cc) → new_glueVBal0(ywv695, ywv696, ywv697, ywv698, ywv699, ywv693, cb, cc)
new_glueVBal3GlueVBal213(ywv563, ywv564, Succ(ywv56500), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Pos(Zero), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(ywv10620), ywv1063, ywv1064, Succ(ywv5880), bd, be) → new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, ywv1064, new_primPlusNat0(ywv5880, ywv10033200), bd, be)
new_glueVBal3GlueVBal27(ywv576, ywv577, Pos(ywv5780), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal20(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, ywv574, ywv56500, h, ba)
new_glueVBal3GlueVBal10(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Succ(ywv57800)), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal29(ywv576, ywv577, ywv57800, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, ywv57800, ywv587, bh, ca)
new_glueVBal3GlueVBal17(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv70400), ywv7190, bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv70400, ywv7190, bb, bc)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Succ(ywv57800)), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal3GlueVBal29(ywv576, ywv577, ywv57800, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, ywv57800, Succ(new_primPlusNat0(ywv5860, ywv587)), bh, ca)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal22(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv704, bb, bc) → new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_sizeFM(Branch(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677), bb, bc), ywv704, bb, bc)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Neg(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal18(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv70400, Zero, bb, bc)
new_glueVBal0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal28(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Succ(ywv106200), ywv1063, ywv1064, ywv595, bd, be) → new_glueVBal3GlueVBal111(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv106200, Succ(ywv595), bd, be)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(ywv5650), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal23(ywv563, ywv564, ywv5650, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Zero, Zero, cb, cc) → new_glueVBal3GlueVBal213(ywv690, ywv691, Succ(ywv692), ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, cb, cc)
new_glueVBal3GlueVBal213(ywv563, ywv564, Zero, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal10(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Succ(ywv7000), Zero, cb, cc) → new_glueVBal3GlueVBal23(ywv690, ywv691, Succ(ywv692), ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, cb, cc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Succ(ywv56100)), bd, be) → new_glueVBal3GlueVBal27(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv56100), ywv56100, bd, be)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Pos(ywv10620), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Succ(ywv5880), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv6830), Succ(ywv6840), bb, bc) → new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv6830, ywv6840, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Succ(ywv56100)), bd, be) → new_glueVBal3GlueVBal2(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv56100), ywv56100, bd, be)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Pos(Zero), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Succ(ywv704000), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(Zero), Pos(Succ(Succ(ywv704000))), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Zero, ywv1063, ywv1064, ywv595, bd, be) → new_glueVBal3GlueVBal112(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv7190), Neg(Zero), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal18(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Succ(Succ(ywv704000)), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Pos(ywv10620), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal3GlueVBal110(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, ywv1064, bd, be)
new_mkBalBranch(ywv1060, ywv1061, ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal21(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal17(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, ywv7190, bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Succ(ywv7000), Succ(ywv7010), cb, cc) → new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, ywv7000, ywv7010, cb, cc)
new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Neg(ywv7100), ywv704, bb, bc) → new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_primMulNat0(ywv7100), ywv704, bb, bc)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv7190), Neg(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv70400, ywv7190, bb, bc)
new_glueVBal3GlueVBal23(ywv563, ywv564, Zero, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal10(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Zero), bd, be) → new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv10033200), bd, be)
new_glueVBal3GlueVBal210(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal214(ywv100330, ywv100331, ywv10033200, Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Zero, bb, bc) → new_glueVBal3GlueVBal25(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, Succ(ywv8000), Succ(ywv8010), bf, bg) → new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, ywv8000, ywv8010, bf, bg)
new_mkBalBranch0(ywv100330, ywv100331, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), ywv100334, bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, Zero, Succ(ywv8010), bf, bg) → new_glueVBal(ywv799, ywv790, ywv791, ywv792, ywv793, ywv794, bf, bg)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal28(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_glueVBal(Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal23(ywv563, ywv564, Succ(ywv56500), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(Zero), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal(ywv1064, ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal22(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal21(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(Succ(ywv71700)), Pos(Succ(Succ(ywv704000))), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv71700, ywv704000, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Zero), bd, be) → new_glueVBal3GlueVBal20(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Zero, Succ(ywv10033200), bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Succ(ywv6840), bb, bc) → new_glueVBal3GlueVBal24(ywv673, ywv674, Succ(ywv675), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal20(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(new_primPlusNat0(ywv5730, ywv574)), ywv56500, h, ba)
new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, Branch(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824), bb, bc) → new_glueVBal3(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824, ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, bb, bc)
new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv71700), Succ(ywv704000), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv71700, ywv704000, bb, bc)
new_glueVBal3GlueVBal212(ywv576, ywv577, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Pos(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal17(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, ywv70400, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal112(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, bd, be) → new_glueVBal(ywv1064, ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be)
new_primPlusNat2(Zero) → Succ(Succ(new_primPlusNat0(new_primPlusNat0(Succ(Zero), Succ(Zero)), Zero)))
new_primPlusNat0(Zero, Zero) → Zero
new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → new_sizeFM0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_primPlusNat2(Succ(ywv5610000)) → Succ(Succ(new_primPlusNat0(Succ(new_primPlusNat0(new_primPlusNat0(Succ(Succ(ywv5610000)), Succ(Succ(ywv5610000))), Succ(ywv5610000))), ywv5610000)))
new_primMulNat(ywv56100) → Succ(Succ(new_primPlusNat1(ywv56100)))
new_primMulNat0(Zero) → Zero
new_sizeFM(EmptyFM, bd, be) → Pos(Zero)
new_sizeFM0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → ywv1062
new_primPlusNat1(Succ(ywv561000)) → Succ(Succ(new_primPlusNat2(ywv561000)))
new_primPlusNat0(Zero, Succ(ywv57400)) → Succ(ywv57400)
new_primPlusNat0(Succ(ywv573000), Zero) → Succ(ywv573000)
new_primPlusNat0(Succ(ywv573000), Succ(ywv57400)) → Succ(Succ(new_primPlusNat0(ywv573000, ywv57400)))
new_primMulNat0(Succ(ywv71000)) → new_primPlusNat0(new_primMulNat(ywv71000), Succ(ywv71000))
new_primPlusNat1(Zero) → Succ(Succ(Zero))
new_sizeFM(Branch(ywv10630, ywv10631, ywv10632, ywv10633, ywv10634), bd, be) → ywv10632
new_sizeFM(EmptyFM, x0, x1)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero)
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)
new_primPlusNat2(Succ(x0))
new_primPlusNat2(Zero)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_primPlusNat1(Succ(x0))
new_primMulNat(x0)
new_primMulNat0(Succ(x0))
new_primMulNat0(Zero)
new_glueVBal3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Zero), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal27(ywv576, ywv577, Pos(ywv5780), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal24(ywv576, ywv577, ywv5780, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca)
new_glueVBal3(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, Branch(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824), Succ(ywv7190), Pos(ywv7040), bb, bc) → new_glueVBal3(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824, ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal10(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal29(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Succ(ywv10033200), Zero, bd, be)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Pos(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Succ(ywv10033200)), Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal25(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc) → new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_glueVBal3Size_l(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc), bb, bc)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Zero), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal212(ywv576, ywv577, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv6830), Zero, bb, bc) → new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_glueVBal3Size_l(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc), bb, bc)
new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Pos(ywv7100), ywv704, bb, bc) → new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_primMulNat0(ywv7100), ywv704, bb, bc)
new_glueVBal3GlueVBal110(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal210(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal21(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal24(ywv576, ywv577, ywv5780, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(Succ(ywv106200)), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal3GlueVBal111(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv106200, ywv10033200, bd, be)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Zero, Succ(ywv7010), cb, cc) → new_glueVBal0(ywv695, ywv696, ywv697, ywv698, ywv699, ywv693, cb, cc)
new_glueVBal3GlueVBal213(ywv563, ywv564, Succ(ywv56500), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Pos(Zero), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(ywv10620), ywv1063, ywv1064, Succ(ywv5880), bd, be) → new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, ywv1064, new_primPlusNat0(ywv5880, ywv10033200), bd, be)
new_glueVBal3GlueVBal27(ywv576, ywv577, Pos(ywv5780), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal20(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, ywv574, ywv56500, h, ba)
new_glueVBal3GlueVBal10(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Succ(ywv57800)), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal29(ywv576, ywv577, ywv57800, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, ywv57800, ywv587, bh, ca)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Succ(ywv57800)), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal3GlueVBal29(ywv576, ywv577, ywv57800, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, ywv57800, Succ(new_primPlusNat0(ywv5860, ywv587)), bh, ca)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal22(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv704, bb, bc) → new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_sizeFM(Branch(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677), bb, bc), ywv704, bb, bc)
new_glueVBal3GlueVBal28(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Succ(ywv106200), ywv1063, ywv1064, ywv595, bd, be) → new_glueVBal3GlueVBal111(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv106200, Succ(ywv595), bd, be)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(ywv5650), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal23(ywv563, ywv564, ywv5650, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Zero, Zero, cb, cc) → new_glueVBal3GlueVBal213(ywv690, ywv691, Succ(ywv692), ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, cb, cc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Succ(ywv56100)), bd, be) → new_glueVBal3GlueVBal27(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv56100), ywv56100, bd, be)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Succ(ywv7000), Zero, cb, cc) → new_glueVBal3GlueVBal23(ywv690, ywv691, Succ(ywv692), ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, cb, cc)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Pos(ywv10620), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Succ(ywv5880), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv6830), Succ(ywv6840), bb, bc) → new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv6830, ywv6840, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Succ(ywv56100)), bd, be) → new_glueVBal3GlueVBal2(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv56100), ywv56100, bd, be)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Pos(Zero), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Succ(ywv704000), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(Zero), Pos(Succ(Succ(ywv704000))), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv7190), Neg(Zero), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Zero, ywv1063, ywv1064, ywv595, bd, be) → new_glueVBal3GlueVBal112(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Pos(ywv10620), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal3GlueVBal110(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal21(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal17(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, ywv7190, bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Succ(ywv7000), Succ(ywv7010), cb, cc) → new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, ywv7000, ywv7010, cb, cc)
new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Neg(ywv7100), ywv704, bb, bc) → new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_primMulNat0(ywv7100), ywv704, bb, bc)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv7190), Neg(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv70400, ywv7190, bb, bc)
new_glueVBal3GlueVBal23(ywv563, ywv564, Zero, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal10(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Zero), bd, be) → new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv10033200), bd, be)
new_glueVBal3GlueVBal210(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Zero, bb, bc) → new_glueVBal3GlueVBal25(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, Succ(ywv8000), Succ(ywv8010), bf, bg) → new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, ywv8000, ywv8010, bf, bg)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal28(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, Zero, Succ(ywv8010), bf, bg) → new_glueVBal(ywv799, ywv790, ywv791, ywv792, ywv793, ywv794, bf, bg)
new_glueVBal(Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal23(ywv563, ywv564, Succ(ywv56500), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal22(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal21(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(Zero), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal(ywv1064, ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(Succ(ywv71700)), Pos(Succ(Succ(ywv704000))), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv71700, ywv704000, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Zero), bd, be) → new_glueVBal3GlueVBal20(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Zero, Succ(ywv10033200), bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Succ(ywv6840), bb, bc) → new_glueVBal3GlueVBal24(ywv673, ywv674, Succ(ywv675), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal20(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(new_primPlusNat0(ywv5730, ywv574)), ywv56500, h, ba)
new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, Branch(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824), bb, bc) → new_glueVBal3(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824, ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, bb, bc)
new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv71700), Succ(ywv704000), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv71700, ywv704000, bb, bc)
new_glueVBal3GlueVBal212(ywv576, ywv577, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Pos(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal17(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, ywv70400, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal112(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, bd, be) → new_glueVBal(ywv1064, ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be)
new_primPlusNat2(Zero) → Succ(Succ(new_primPlusNat0(new_primPlusNat0(Succ(Zero), Succ(Zero)), Zero)))
new_primPlusNat0(Zero, Zero) → Zero
new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → new_sizeFM0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_primPlusNat2(Succ(ywv5610000)) → Succ(Succ(new_primPlusNat0(Succ(new_primPlusNat0(new_primPlusNat0(Succ(Succ(ywv5610000)), Succ(Succ(ywv5610000))), Succ(ywv5610000))), ywv5610000)))
new_primMulNat(ywv56100) → Succ(Succ(new_primPlusNat1(ywv56100)))
new_primMulNat0(Zero) → Zero
new_sizeFM(EmptyFM, bd, be) → Pos(Zero)
new_sizeFM0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → ywv1062
new_primPlusNat1(Succ(ywv561000)) → Succ(Succ(new_primPlusNat2(ywv561000)))
new_primPlusNat0(Zero, Succ(ywv57400)) → Succ(ywv57400)
new_primPlusNat0(Succ(ywv573000), Zero) → Succ(ywv573000)
new_primPlusNat0(Succ(ywv573000), Succ(ywv57400)) → Succ(Succ(new_primPlusNat0(ywv573000, ywv57400)))
new_primMulNat0(Succ(ywv71000)) → new_primPlusNat0(new_primMulNat(ywv71000), Succ(ywv71000))
new_primPlusNat1(Zero) → Succ(Succ(Zero))
new_sizeFM(Branch(ywv10630, ywv10631, ywv10632, ywv10633, ywv10634), bd, be) → ywv10632
new_sizeFM(EmptyFM, x0, x1)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero)
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)
new_primPlusNat2(Succ(x0))
new_primPlusNat2(Zero)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_primPlusNat1(Succ(x0))
new_primMulNat(x0)
new_primMulNat0(Succ(x0))
new_primMulNat0(Zero)
new_glueVBal3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Zero), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal27(ywv576, ywv577, Pos(ywv5780), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal24(ywv576, ywv577, ywv5780, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca)
new_glueVBal3(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, Branch(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824), Succ(ywv7190), Pos(ywv7040), bb, bc) → new_glueVBal3(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824, ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal10(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal29(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Succ(ywv10033200), Zero, bd, be)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Pos(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Succ(ywv10033200)), Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal25(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc) → new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_glueVBal3Size_l(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc), bb, bc)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Zero), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal212(ywv576, ywv577, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv6830), Zero, bb, bc) → new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_glueVBal3Size_l(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc), bb, bc)
new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Pos(ywv7100), ywv704, bb, bc) → new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_primMulNat0(ywv7100), ywv704, bb, bc)
new_glueVBal3GlueVBal110(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal210(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal21(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal24(ywv576, ywv577, ywv5780, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(Succ(ywv106200)), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal3GlueVBal111(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv106200, ywv10033200, bd, be)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Zero, Succ(ywv7010), cb, cc) → new_glueVBal0(ywv695, ywv696, ywv697, ywv698, ywv699, ywv693, cb, cc)
new_glueVBal3GlueVBal213(ywv563, ywv564, Succ(ywv56500), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Pos(Zero), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(ywv10620), ywv1063, ywv1064, Succ(ywv5880), bd, be) → new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, ywv1064, new_primPlusNat0(ywv5880, ywv10033200), bd, be)
new_glueVBal3GlueVBal27(ywv576, ywv577, Pos(ywv5780), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal20(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, ywv574, ywv56500, h, ba)
new_glueVBal3GlueVBal10(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Succ(ywv57800)), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Zero, ywv587, bh, ca) → new_glueVBal3GlueVBal29(ywv576, ywv577, ywv57800, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, ywv57800, ywv587, bh, ca)
new_glueVBal3GlueVBal27(ywv576, ywv577, Neg(Succ(ywv57800)), ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, Succ(ywv5860), ywv587, bh, ca) → new_glueVBal3GlueVBal29(ywv576, ywv577, ywv57800, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, ywv57800, Succ(new_primPlusNat0(ywv5860, ywv587)), bh, ca)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal22(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal11(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv704, bb, bc) → new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_sizeFM(Branch(ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677), bb, bc), ywv704, bb, bc)
new_glueVBal3GlueVBal28(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Branch(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334), bd, be) → new_glueVBal3GlueVBal26(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be), bd, be)
new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Succ(ywv106200), ywv1063, ywv1064, ywv595, bd, be) → new_glueVBal3GlueVBal111(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv106200, ywv1063, ywv1064, ywv106200, Succ(ywv595), bd, be)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(ywv5650), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Zero, ywv574, h, ba) → new_glueVBal3GlueVBal23(ywv563, ywv564, ywv5650, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Zero, Zero, cb, cc) → new_glueVBal3GlueVBal213(ywv690, ywv691, Succ(ywv692), ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, cb, cc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Succ(ywv56100)), bd, be) → new_glueVBal3GlueVBal27(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv56100), ywv56100, bd, be)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Succ(ywv7000), Zero, cb, cc) → new_glueVBal3GlueVBal23(ywv690, ywv691, Succ(ywv692), ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, cb, cc)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Pos(ywv10620), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Succ(ywv5880), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv6830), Succ(ywv6840), bb, bc) → new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv6830, ywv6840, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Succ(ywv56100)), bd, be) → new_glueVBal3GlueVBal2(ywv100330, ywv100331, ywv100332, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv56100), ywv56100, bd, be)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), Pos(Zero), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Succ(ywv704000), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(Zero), Pos(Succ(Succ(ywv704000))), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv7190), Neg(Zero), bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal19(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Zero, ywv1063, ywv1064, ywv595, bd, be) → new_glueVBal3GlueVBal112(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Pos(ywv10620), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal3GlueVBal110(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv10620, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Zero), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal21(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal17(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, ywv7190, bb, bc) → new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, Succ(ywv7000), Succ(ywv7010), cb, cc) → new_glueVBal3GlueVBal29(ywv690, ywv691, ywv692, ywv693, ywv694, ywv695, ywv696, ywv697, ywv698, ywv699, ywv7000, ywv7010, cb, cc)
new_glueVBal3GlueVBal12(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Neg(ywv7100), ywv704, bb, bc) → new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, new_primMulNat0(ywv7100), ywv704, bb, bc)
new_glueVBal3GlueVBal14(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv7190), Neg(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv70400, ywv7190, bb, bc)
new_glueVBal3GlueVBal23(ywv563, ywv564, Zero, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal10(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Zero), bd, be) → new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, new_primMulNat(ywv10033200), bd, be)
new_glueVBal3GlueVBal210(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, Pos(Succ(ywv106200)), ywv1063, Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Zero), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Zero, bb, bc) → new_glueVBal3GlueVBal25(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, Succ(ywv8000), Succ(ywv8010), bf, bg) → new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, ywv8000, ywv8010, bf, bg)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Zero), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Neg(Zero), bd, be) → new_glueVBal3GlueVBal28(ywv100330, ywv100331, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_glueVBal3GlueVBal111(ywv790, ywv791, ywv792, ywv793, ywv794, ywv795, ywv796, ywv797, ywv798, ywv799, Zero, Succ(ywv8010), bf, bg) → new_glueVBal(ywv799, ywv790, ywv791, ywv792, ywv793, ywv794, bf, bg)
new_glueVBal(Branch(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644), ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be) → new_glueVBal3(ywv10640, ywv10641, ywv10642, ywv10643, ywv10644, ywv100330, ywv100331, Neg(Succ(ywv10033200)), ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal23(ywv563, ywv564, Succ(ywv56500), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal22(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba) → new_glueVBal3GlueVBal21(ywv563, ywv564, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, h, ba)
new_glueVBal3GlueVBal1(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, Neg(Zero), ywv1063, ywv1064, Zero, bd, be) → new_glueVBal(ywv1064, ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(Succ(ywv71700)), Pos(Succ(Succ(ywv704000))), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv71700, ywv704000, bb, bc)
new_glueVBal3GlueVBal26(ywv100330, ywv100331, Pos(Succ(ywv10033200)), ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Pos(Zero), bd, be) → new_glueVBal3GlueVBal20(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, Zero, Succ(ywv10033200), bd, be)
new_glueVBal3GlueVBal20(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Succ(ywv6840), bb, bc) → new_glueVBal3GlueVBal24(ywv673, ywv674, Succ(ywv675), ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Pos(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal20(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(new_primPlusNat0(ywv5730, ywv574)), ywv56500, h, ba)
new_glueVBal3GlueVBal16(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, Branch(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824), bb, bc) → new_glueVBal3(ywv6820, ywv6821, ywv6822, ywv6823, ywv6824, ywv673, ywv674, Pos(Succ(ywv675)), ywv676, ywv677, bb, bc)
new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Succ(ywv71700), Succ(ywv704000), bb, bc) → new_glueVBal3GlueVBal15(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, ywv71700, ywv704000, bb, bc)
new_glueVBal3GlueVBal212(ywv576, ywv577, ywv579, ywv580, ywv581, ywv582, ywv583, ywv584, ywv585, bh, ca) → new_glueVBal0(ywv581, ywv582, ywv583, ywv584, ywv585, ywv579, bh, ca)
new_glueVBal3GlueVBal13(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, Pos(Succ(ywv70400)), bb, bc) → new_glueVBal3GlueVBal17(ywv673, ywv674, ywv675, ywv676, ywv677, ywv678, ywv679, ywv680, ywv681, ywv682, Zero, ywv70400, bb, bc)
new_glueVBal3GlueVBal2(ywv563, ywv564, Neg(Succ(ywv56500)), ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, Succ(ywv5730), ywv574, h, ba) → new_glueVBal3GlueVBal1(ywv563, ywv564, ywv56500, ywv566, ywv567, ywv568, ywv569, ywv570, ywv571, ywv572, new_primMulNat(ywv56500), h, ba)
new_glueVBal3GlueVBal112(ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, ywv1060, ywv1061, ywv1063, ywv1064, bd, be) → new_glueVBal(ywv1064, ywv100330, ywv100331, ywv10033200, ywv100333, ywv100334, bd, be)
new_primMulNat(ywv56100) → Succ(Succ(new_primPlusNat1(ywv56100)))
new_primPlusNat1(Succ(ywv561000)) → Succ(Succ(new_primPlusNat2(ywv561000)))
new_primPlusNat1(Zero) → Succ(Succ(Zero))
new_primPlusNat2(Zero) → Succ(Succ(new_primPlusNat0(new_primPlusNat0(Succ(Zero), Succ(Zero)), Zero)))
new_primPlusNat2(Succ(ywv5610000)) → Succ(Succ(new_primPlusNat0(Succ(new_primPlusNat0(new_primPlusNat0(Succ(Succ(ywv5610000)), Succ(Succ(ywv5610000))), Succ(ywv5610000))), ywv5610000)))
new_primPlusNat0(Succ(ywv573000), Succ(ywv57400)) → Succ(Succ(new_primPlusNat0(ywv573000, ywv57400)))
new_primPlusNat0(Zero, Succ(ywv57400)) → Succ(ywv57400)
new_primPlusNat0(Succ(ywv573000), Zero) → Succ(ywv573000)
new_primPlusNat0(Zero, Zero) → Zero
new_glueVBal3Size_l(ywv1003330, ywv1003331, ywv1003332, ywv1003333, ywv1003334, ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → new_sizeFM0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be)
new_sizeFM0(ywv1060, ywv1061, ywv1062, ywv1063, ywv1064, bd, be) → ywv1062
new_primMulNat0(Zero) → Zero
new_primMulNat0(Succ(ywv71000)) → new_primPlusNat0(new_primMulNat(ywv71000), Succ(ywv71000))
new_sizeFM(Branch(ywv10630, ywv10631, ywv10632, ywv10633, ywv10634), bd, be) → ywv10632
new_sizeFM(EmptyFM, x0, x1)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero)
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)
new_primPlusNat2(Succ(x0))
new_primPlusNat2(Zero)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_primPlusNat1(Succ(x0))
new_primMulNat(x0)
new_primMulNat0(Succ(x0))
new_primMulNat0(Zero)
new_glueVBal3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
new_minusFM(Branch(ywv30, ywv31, ywv32, ywv33, ywv34), Branch(ywv40, ywv41, ywv42, ywv43, ywv44), h, ba) → new_minusFM(new_splitLT2(ywv30, ywv31, ywv32, ywv33, ywv34, ywv40, h), ywv43, h, ba)
new_minusFM(Branch(ywv30, ywv31, ywv32, ywv33, ywv34), Branch(ywv40, ywv41, ywv42, ywv43, ywv44), h, ba) → new_minusFM(new_splitGT2(ywv30, ywv31, ywv32, ywv33, ywv34, ywv40, h), ywv44, h, ba)
new_splitLT2(@0, ywv31, ywv32, ywv33, ywv34, @0, h) → ywv33
new_splitGT2(@0, ywv31, ywv32, ywv33, ywv34, @0, h) → ywv34
new_splitGT2(@0, x0, x1, x2, x3, @0, x4)
new_splitLT2(@0, x0, x1, x2, x3, @0, x4)
From the DPs we obtained the following set of size-change graphs: